forall a: forall b:
L:a,b;L:b = L:a,b